1. Technical Field
The present invention relates in general to testing and verification, and in particular to verification of digital designs. Still more particularly, the present invention relates to a system, method and computer program product for verification of digital designs via comparison of results from operational and reference models.
2. Description of the Related Art
With the increasing penetration of processor-based systems into every facet of human activity, demands have increased on the processor and application-specific integrated circuit (ASIC) development and production community to produce systems that are free from design flaws. Circuit products, including microprocessors, digital signal and other special-purpose processors, and ASICs, have become involved in the performance of a vast array of critical functions, and the involvement of microprocessors in the important tasks of daily life has heightened the expectation of error-free and flaw-free design. Whether the impact of errors in design would be measured in human lives or in mere dollars and cents, consumers of circuit products have lost tolerance for results polluted by design errors. Consumers will not tolerate, by way of example, miscalculations on the floor of the stock exchange, in the medical devices that support human life, or in the computers that control their automobiles. All of these activities represent areas where the need for reliable circuit results has risen to a mission-critical concern.
In response to the increasing need for reliable, error-free designs, the processor and ASIC design and development community has developed rigorous, if incredibly expensive, methods for testing and verification. Simulation has been a traditional method for verifying such complex designs as processor chips. Because the simulation time for a design grows, in the worst case, in relation to the number of logic elements, simulation and verification of complex systems is one of the most time-consuming computing tasks today. It is therefore important to use simulation cycles effectively, with the aim that few bugs escape and development time is reduced.
Traditionally, floating point units (FPUs) of processors are validated by simulation, often using targeted techniques such as specialized testcase generators. While such approaches are efficient at exposing many bugs, they are based on incomplete methods, which cannot achieve full coverage, (i.e., evaluation of all operand combinations over all rounding modes and exception states). To compound the coverage problem, designs face shorter time-to-market (hence less verification time) from generation to generation, require higher clock speeds and thus a larger degree of pipelining, and acquire additional features such as clock gating for low-power. Formal and semiformal verification techniques constitute an increasingly prevalent mechanism by which to attempt to close the coverage gap imposed by simulation. For example, numerous approaches have proposed the use of a combination of automatic methods and manual theorem-proving techniques to yield complete proofs of correctness of FPUs.
There are three building blocks in the FPU that are major hurdles for the formal algorithms: namely, the multiplier, the alignment shifter that aligns the addend to the product, and the normalization shifter that eliminates leading zeros in the intermediate result before rounding. In testing, verification of each of these building blocks leads to run-time explosion of the symbolic models of the processor, and memory-explosion of binary decision diagrams representing the processor's symbolic logic.
What is needed is a more efficient method for verifying floating-point units, in particular, and more generally for verifying a digital design utilizing a simulation model.